『［2021CAPE公開セミナー］論理学上級 Ⅱ-3 証明論的意味論としてのマーティン・レーフの構成的型理論』
矢田部 俊介. [2021CAPE公開セミナー] 論理学上級 Ⅱ-3「証明論的意味論としてのマーティン・レーフの構成的型理論」. 2021. https://www.youtube.com/watch?v=CPv4KjpTpgQ
Σ型⇄∃
Π型⇄∀
命題と判断図式
概念、観念
感性
総合的判断
知識は増える
分析的判断
知識は増えない
直観
「雪は白い」という判断の正当性は感性によって得られる観測データによって支えられる
直観主義論理
カントの意味の直観
トポロジーの分野を作った人でもある
証明のデータ型としての命題
構成と解体(construction and deconstruction)
帰納的定義
最初のステップ(initial step/base step)
後続ステップ(successor step/induction step)
構成子(constructor)
自然数の構成
$ \bar{0} は$ L_0 の個体番号
引数0の構成子
$ S は$ L_0 の関数番号
引数1の構成子
$ N = \begin{cases} \bar{0} \\ S(x) : N & (x:N) \end{cases}
多分うまく定義を書けていない
解体子
前者関数$ \mathrm{pred} を定義
$ \mathrm{pred}(\bar{0}) = \bar{0}
$ \mathrm{pred}(S(\bar{0})) = \bar{n}
構成子
解体子
関連